\section{Evolving Systems}
\label{sec:Evolving}

The File System of \Fig \ref{fig:naivefs} was not ensuring any property we were interested in. This Section presents two interesting iterations: the first step leads to a \emph{simple File System} $\FSS$ that matches Requirement \textbf{\texttt{R1}}, \ie files can be opened only by users with sufficient access rights; the second iteration leads to a \emph{Confined File System} $\FSC$ that matches Requirement \textbf{\texttt{R2}}, \ie it further ensures the confinement property on file opening. 

The additional abstract data types for each version of the \textsc{Fs} as well as the precise definition of the required morphisms to ensure a correct iteration can be found in \cite{lucio:10}.

\subsection{Simple File System \emph{$\FSS$}}
\label{sec:Evolving-Simple}

\begin{figure}[t]
	\centering
  \epsfig{file=images/simple_security_fs, width=\linewidth}
	\caption{Simple security filesystem. Same initial marking as \Fig\ref{fig:naivefs}.}
	\label{fig:simplesec}

	%\vspace{-0.4cm}
\end{figure}

The \textsc{Fs} of \Fig \ref{fig:MLS-M} was naive in the sense that it simply implements the basic mechanisms for opening / reading and closing files, without access control. We make $\FS$ evolve into $\FSS$ to meet Requirement \textbf{\texttt{R1}} by guarding each file use (either reading or writing) by a condition that checks the access rights: in \Fig \ref{fig:simplesec}, each transition ($\mathtt{openR}$, $\mathtt{openW}$, $\mathtt{closeR}$ or $\mathtt{closeW}$) is now guarded to prevent the firing if the $\mathtt{\$u}$'s access class does not dominate $\mathtt{\$f}$'s access class. 

In this iteration, the \textsc{Pn}'s structure does not change (\ie no places are added or removed), but the transitions are strengthened by new guards that straightforwardly imply the previous empty guards. The iteration is however safe because an (identity) morphism still exists from $\FS$ to $\FSS$. Table \ref{tab:satisfaction} (Row 2) summarizes the iteration when model-checking all properties on $\FSS$: $\mathtt{P1}$ and $\mathtt{P2}$ now hold.


\subsection{Confined File System \emph{$\FSC$}}
\label{sec:Evolving-Confined}

We now make $\FSS$ evolve into $\FSC$ to prevent Trojan horses attacks happening, thus meeting Requirement \textbf{\texttt{R2}}. Two new places $\mathtt{logRead}$ and $\mathtt{logWrite}$ are added: they log a list of pairs $(\mathtt{\$f}, \mathtt{\$u})$, adding an element each time $\mathtt{\$u}$ opens $\mathtt{\$f}$ and deleting it when closed, for each opening mode. Every time a \emph{new} file is opened in read mode, $\mathtt{openRead}$ checks from $\mathtt{logWrite}$ if no file with smaller access rights is open by the same user in write mode. We introduce a new function $\mathtt{min(\$lfu)}$ that computes the minimum access class (for the domination) in the list $\mathtt{\$lfu}$ of pairs $(\mathtt{\$f}, \mathtt{\$u})$. The new guard for the $\mathtt{openRead}$ transition is now a conjunction of the previous guard with a new condition stating that the minimal access class in $\mathtt{logWrite}$ dominates the newly opened file. The reverse principle is applied for $\mathtt{openWrite}$ with a function $\mathtt{max}$ retrieving the maximal access class logged in $\mathtt{logRead}$.

In this iteration, two new places were added (namely, $\mathtt{logRead}$ and $\mathtt{logWrite}$), and the guards for two transitions (namely, $\mathtt{openR}$ and $\mathtt{openW}$) were strengthen with a new condition. These constitute a safe iteration from $\FSS$ to $\FSC$ because the corresponding morphisms match the conditions of \Sect \ref{sec:Preservation}. Table \ref{tab:satisfaction} (Row 3) summarizes the model-checking of all properties on $\FSC$: $\mathtt{P1}$ and $\mathtt{P2}$ still hold; $\mathtt{P3}$ is now satisfied.


\begin{figure}[t]
	\centering
  \epsfig{file=images/confined_fs, width=\linewidth}
	\caption{Confined filesystem. Same initial marking as \Fig\ref{fig:naivefs}.}
	\label{fig:confinedfs}

%\vspace{-0.4cm}
\end{figure}
